Internet of Things (IoT) devices promote the rapid development of cloud storage outsourcing data service, which is favored by more and more terminal users. Therefore, how to ensure the integrity verification of user data in cloud server has become a hot issue that needs to be solved urgently. For resource-constrained users, current cloud data audit scheme has the problems such as complex computation, high cost and low efficiency. To solve these problems, an efficient dynamic data audit scheme for resource-constrained users was proposed. First, a new data structure was proposed based on Novel Counting Bloom Filter (NCBF) and Multi-Merkle Hash Tree (M-MHT) to support dynamic audit, namely NCBF-M-MHT. In this data structure, the NCBF structure was able to realize the dynamic updating request of data within O(1) time, thereby ensuring the efficiency of audit. And the root node of M-MHT structure performed signing by user authentication to ensure the security of data. Then, different allocation methods were adopted for different audit entities, and the data evidence and label evidence were used to verify the correctness and integrity of data. Experimental results show that compared with the audit scheme based on Dynamic Hash Table (DHT), the audit scheme based on Merkle Hash Tree (MHT) and the audit scheme based on Location Array-Doubly Linked Info Table (LA-DLIT), the time cost of the proposed scheme in the audit verification phase is reduced by 45.40%, 23.71% and 13.85%, and the time cost in the dynamic update phase is reduced by 43.33%, 27.50% and 17.58% respectively.

Concerning the problems and challenges in Cyber Physical System (CPS), a new modeling and verification method of CPS was proposed based on service composition ideas. Firstly, a composition structure of CPS was proposed, including the physical world, sensor systems, information processing systems, control systems and time constraints. Based on this proposed structure, the service classification and composition framework of CPS resources were proposed. The physical environment modeling, atomic service modeling and service composition of CPS were also given based on the timed automata theory. Finally, through case design and model checking tool Uppaal, the experimental results were given to illustrate the correctness of the CPS service-oriented modeling approach, including system security, accessibility, liveness and time constraints. The results verify the above properties and the correctness of the proposed method.